#ifndef CINTA_H
#define CINTA_H
#include "tuple.h"
#include "bool.h"

typedef struct celda * aList;
typedef struct sCinta * Cinta;

aList
aList_vacia(void);
/*Desc: Constructor de lista vacia */

aList
aList_destroy(aList l);
/*Desc: Destruyre todos los elementos de la lista (vacia o no) */

Cinta
cinta_create(aList l);
/*
DESC: Constructor de cinta.
PRE: { l = L }
  c = cinta_create(l);
POS: { Pi(c) ++ Pd(c) = L }
*/

void
cinta_arr(Cinta c);
/*
DESC: Arranca la cinta.
PRE: { L = Pi(c) ++ Pd(c) }
   cinta_arr(c);
POS: { Pi(c)=[] /\ Pd(c)=L }
*/

Bool
cinta_fin(Cinta c);
/*
DESC: Pregunta si llego al final.
DEF: cinta_fin(c) == (Pd(c) = [])
*/

void
cinta_av(Cinta c);
/*
DESC: Avanza la cinta.
PRE: { Pi(c) = L1 /\ Pd(c) = e:L2 }
   cinta_av(c);
POS: { Pi(c)=L1:e /\ Pd(c)=L2 }
*/

Tuple
cinta_elec(Cinta c);
/*
DESC: Elemento corriente de la cinta.
DEF: Pd(c) /= [] ==> cinta_elec(c) = head(Pd(c))
*/

void
cinta_ins(Cinta c, Tuple t);
/*
DESC: inserta una tupla.
PRE: { t= T; Pi(c) = L1 /\ Pd(c) = L2 }
   cinta_ins(c,t);
POS: { t=T /\ Pi(c)=L1 /\ Pd(c)=t:L2 }
*/

void
cinta_del(Cinta c);
/*
DESC: Borra el elemento corriente.
PRE: { Pi(c) = L1 /\ Pd(c) = e:L2 }
   cinta_del(c);
POS: { Pi(c)=L1 /\ Pd(c)=L2 }
*/

aList
cinta_destroy(Cinta c);
/*
DESC: Destructor.
PRE: { Pi(c) = L1 /\ Pd(c) = L2 }
   l = cinta_destroy(c);
POS: { l = Pi(c)++ Pd(c) }
*/

#endif
